import os
import simsym
import symtypes
import errno
import model
import signal

maxprocs = simsym.SInt.var("maxprocs")

NullProcRef = 0
IdleProcRef = maxprocs

class PREF(simsym.SInt):
	def _declare_assumptions(self, assume):
		super(PREF, self)._declare_assumptions(assume)
		assume(simsym.symand([self >= NullProcRef, self <= IdleProcRef]))

class IPREF(PREF):
	def _declare_assumptions(self, assume):
		super(IPREF, self)._declare_assumptions(assume)
		assume(self != NullProcRef)
class APREF(IPREF):
	def _declare_assumptions(self, assume):
		super(IPREF, self)._declare_assumptions(assume)
		assume(self != IdleProcRef)


class MEMDESC(simsym.tstruct(p = simsym.SInt, size = simsym.SInt)):
	def _declare_assumptions(self, assume):
		super(MEMDESC, self)._declare_assumptions(assume)


def hole_size(mem):
	return mem.size

PSTACK		= simsym.tsynonym("PSTACK", MEMDESC)
PDATA		= simsym.tsynonym("PDATA", MEMDESC)
PCODE		= simsym.tsynonym("PCODE", MEMDESC)

PRIO		= simsym.tsynonym("PRIO", simsym.SInt)

pstnew		= 1
pstrunning	= 2
pstready	= 3
pstwaiting	= 4
pstterm		= 5

class PROCSTATUS(simsym.SInt):
	def _declare_assumptions(self, assume):
		super(PROCSTATUS, self)._declare_assumptions(assume)
		assume(simsym.symand([self >= 1, self <= 5]))


STATUSWD	= simsym.tsynonym("STATUSWD", simsym.SInt)

MSGDATA		= simsym.tuninterpreted("MSGDATA")
MSGSRC		= simsym.tsynonym("MSGSRC", APREF) # or Hardware

Hardware = -1
class MSGSRC(simsym.SInt):
	def _declare_assumptions(self, assume):
		super(MSGSRC, self)._declare_assumptions(assume)
		assume(simsym.symor(
				[simsym.symand([self > NullProcRef, self < IdleProcRef]),
				self == Hardware]))

MBOXMSG		= simsym.tstruct(src = MSGSRC, msg = MSGDATA)

SEMAID		= simsym.tsynonym("SEMAID", simsym.SInt)

currentp	= APREF.var("currentp")


class LowLevelScheduler(simsym.tstruct(
		tmp = simsym.SInt
		)):
	def _declare_assumptions(self, assume):
		super(LowLevelScheduler, self)._declare_assumptions(assume)
	
	@model.methodwrap()
	def CurrentProcess(self):
		return currentp
	
	@model.methodwrap(p = APREF)
	def makeUnready(self, p):
		pass
	
	@model.methodwrap()
	def ScheduleNext(self):
		pass

	
